DROPS

Document

DOI: 10.4230/LIPIcs.CP.2023.26

Proof Logging for Smart Extensional Constraints

Authors: Matthew J. McIlree and Ciaran McCreesh

Published in: LIPIcs, Volume 280, 29th International Conference on Principles and Practice of Constraint Programming (CP 2023)

Abstract

Proof logging provides an auditable way of guaranteeing that a solver has produced a correct answer using sound reasoning. This is standard practice for Boolean satisfiability solving, but for constraint programming, a challenge is that every propagator must be able to justify all inferences it performs. Here we demonstrate how to support proof logging for a wide range of previously uncertified global constraints. We do this by showing how to justify every inference that could be performed by the propagation algorithms for two families of generalised extensional constraint: "Smart Table" and "Regular Language Membership".

Cite as

Matthew J. McIlree and Ciaran McCreesh. Proof Logging for Smart Extensional Constraints. In 29th International Conference on Principles and Practice of Constraint Programming (CP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 280, pp. 26:1-26:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{mcilree_et_al:LIPIcs.CP.2023.26,
  author =	{McIlree, Matthew J. and McCreesh, Ciaran},
  title =	{{Proof Logging for Smart Extensional Constraints}},
  booktitle =	{29th International Conference on Principles and Practice of Constraint Programming (CP 2023)},
  pages =	{26:1--26:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-300-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{280},
  editor =	{Yap, Roland H. C.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2023.26},
  URN =		{urn:nbn:de:0030-drops-190633},
  doi =		{10.4230/LIPIcs.CP.2023.26},
  annote =	{Keywords: Constraint programming, proof logging, extensional constraints}
}

Search Results

Documents authored by McIlree, Matthew J.

Proof Logging for Smart Extensional Constraints

Abstract

Cite as

Thanks for your feedback!

Could not send message